#include <intrin.h>
inline unsigned __int64 rdtsc(void)
{
  return __rdtsc();
}

